Nuprl Lemma : send_onceR_wf
0,22
postcript
pdf
T
,
A
:Type,
f
:(
A
T
),
l
:IdLnk.
Normal(
A
)
Normal(
T
)
send_onceR{done:ut2, tg:ut2, b:ut2, done1:ut2}(
T
;
A
;
f
;
l
)
Realizer
latex
Definitions
onceR{$a:ut2, $done:ut2}(
i
)
,
Top
,
true
,
if
b
t
else
f
fi
,
Prop
,
P
Q
,
DeclaredType(
ds
;
x
)
,
s
.
x
,
send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(
T
;
A
;
f
;
l
)
,
x
.
t
(
x
)
,
t
T
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
State(
ds
)
,
Id
,
Normal(
T
)
,
x
(
s
)
,
State(
ds
)
Lemmas
eqof
eq
btrue
,
Rpre
wf
,
Rlist
wf
,
deq
wf
,
subtype
rel
self
,
fpf-cap-single
,
Rinit
wf
,
Rframe
wf
,
id-deq
wf
,
Rsends
wf
,
Id
wf
,
btrue
wf
,
Reffect
wf
,
normal-type
wf
,
IdLnk
wf
,
fpf-cap-single1
,
fpf-single
wf
origin
T, A:Type, f:(A
T), l:IdLnk.
Normal(T)
send_onceR{done:ut2, tg:ut2, b:ut2, done1:ut2}(T; A; f; l) 
Realizer T, A:Type, f:(AT), l:IdLnk.
Normal(T)
send_onceR{done:ut2, tg:ut2, b:ut2, done1:ut2}(T; A; f; l) Realizer 
t else f fi